명제 논리
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.
- 1. 개요
- 2. 정의
- 3. 성질
- 4. 역사
- 5. 문장 (Sentences)
- 6. 논증 (Arguments)
- 7. 형식화 (Formalization)
- 8. 언어 (Language)
- 9. 의미론 (Semantics)
- 10. 증명 체계 (Proof systems)
- 11. 진리표를 통한 의미론적 증명 (Semantic proof via truth tables)
- 12. 의미 표를 통한 의미론적 증명 (Semantic proof via tableaux)
- 13. 자연 연역을 통한 구문적 증명 (Syntactic proof via natural deduction)
- 14. 공리를 통한 구문적 증명 (Syntactic proof via axioms)
- 15. 더 높은 논리 수준 (Higher logical levels)
- 16. 관련 주제 (Related topics)
- 참조
1. 개요
명제 논리는 명제의 참/거짓을 다루는 형식적 추론 체계로, 명제를 논리 연산자를 통해 관계 지어 추론하는 데 초점을 맞춘다. 언어는 명제 변수와 논리 연산자로 구성되며, 잘 구성된 공식과 추론 규칙, 공리를 통해 증명 체계를 구성한다. 진리표, 의미 표, 자연 연역, 공리계 등 다양한 증명 방법이 있으며, 고전 논리에서는 모든 명제가 참 또는 거짓의 진리값을 가지는 이중값 원리를 따른다. 명제 논리는 건전성, 완전성, 콤팩트성을 만족하며, 부울 대수, 일차 논리, 양상 논리 등 다양한 관련 주제와 더 높은 수준의 논리로 확장될 수 있다.
더 읽어볼만한 페이지
- 명제 논리 - 모순
모순은 논리학, 철학, 과학 등 다양한 분야에서 사용되는 개념으로, 서로 상반되는 두 가지 주장이나 사실이 동시에 존재하는 상태를 의미하며, 특히 헤겔과 마르크스의 변증법적 유물론에서 사물의 내재적 대립으로서 역사 발전의 원동력으로 간주된다. - 명제 논리 - 추론 규칙
추론 규칙은 전제가 참일 때 결론이 필연적으로 참임을 보이는 논리적 도출 과정을 형식적으로 표현한 규칙으로, 다양한 유형이 존재하며 명제 논리와 술어 논리에서 기본적인 추론을 수행하는 데 사용되고, 형식 체계의 핵심 요소이다. - 고전 논리 - 동일성
동일성은 철학에서 자기 자신과 일치하고 자기 동일적으로 존재하며 다른 것에 의존하지 않는 개념으로, 고대부터 현대까지 다양한 철학자와 여러 분야에서 논의되고 활용되어 왔다. - 고전 논리 - 논리식
논리식은 논리 체계 내에서 원자 논리식에 논리 연산을 적용하여 얻어지는 문자열이며, 형식 논리에서 수학적 증명을 표현하는 데 사용되는 구문론적 대상으로, 해석을 통해 의미가 부여되고 다양한 속성을 가진다. - 글로벌세계대백과를 인용한 문서/{{{분류 - 공 (악기)
공은 금속으로 제작된 타악기로, 다양한 문화권에서 의식, 신호, 음악 연주 등에 사용되며, 형태와 용도에 따라 여러 종류로 나뉜다. - 글로벌세계대백과를 인용한 문서/{{{분류 - 국무회의
국무회의는 대한민국 대통령을 의장으로, 예산, 법률안, 외교, 군사 등 국정 현안을 심의하는 중요한 기관이며, 대통령, 국무총리, 국무위원으로 구성되고, 정례회의는 매주 1회, 임시회의는 필요에 따라 소집된다.
명제 논리 | |
---|---|
명제 논리 | |
로마자 표기 | myeongje nonli |
종류 | 논리학 |
하위 분야 | 명제 분석, 술어 논리 |
개요 | |
설명 | 명제와 논리적 연결사(connective)를 사용하여 명제 간의 관계를 다루는 논리 체계이다. |
특징 | 명제의 내부 구조를 고려하지 않고, 명제 전체를 하나의 단위로 취급한다. 명제 사이의 논리적 관계를 분석하고, 명제의 진리값을 결정하는 데 사용된다. 간단하고 효율적인 논리 체계이지만, 표현력에 한계가 있다. |
구성 요소 | |
명제 변수 | 명제를 나타내는 기호 (예: p, q, r) |
논리 연결사 | 부정 (¬, not) 논리곱 (∧, and) 논리합 (∨, or) 함의 (→, if...then) 쌍방조건 (↔, if and only if) |
진리표 | |
정의 | 논리 연결사의 모든 가능한 진리값 조합을 표로 나타낸 것 |
활용 | 명제의 진리값을 결정하고, 논리적 타당성을 검증하는 데 사용된다. |
형식 체계 | |
설명 | 명제 논리의 추론 규칙과 공리를 명확히 정의한 체계 |
종류 | 힐베르트 체계 자연 연역 시퀀트 미적분 |
응용 | |
분야 | 컴퓨터 과학, 인공지능, 수학, 철학 |
활용 | 회로 설계, 소프트웨어 검증, 지식 표현, 논리적 추론 |
역사 | |
기원 | 고대 그리스 시대부터 시작되었지만, 19세기 말에 프레게에 의해 현대적인 형태로 발전되었다. |
기타 | |
관련 용어 | 논리 명제 술어 논리 논리적 동치 논리적 귀결 |
2. 정의
명제 논리는 명제 변수와 논리 연산자를 사용하여 명제를 표현하고, 이들 사이의 관계를 탐구하는 논리 체계이다. 명제 논리에서 중요한 것은 개별 명제의 의미보다는, "그리고", "만약 ~이면" 과 같은 논리 연산자로 연결된 명제들 사이의 추론 관계이다.
명제 논리는 일반적으로 명제 변수를 원자식으로 하는 형식적 추론 체계를 통해 이루어진다.[119] 이러한 체계는 "문법적으로 괜찮은" 표현(정식)의 집합, 공리의 집합, 그리고 표현들 간의 변형 규칙으로 구성된다.
표현의 변형 규칙은 의미 동등성을 유지하도록 주어지며, 특히 논리 체계에서는 논리적 동등성을 가리키도록 주어진다. 이를 통해 주어진 표현에서 논리적으로 동등한 표현을 도출하거나, 표현을 단순화하거나, 주어진 표현이 특정 공리와 동등한지 결정하는 등의 문제를 다룰 수 있다.
명제 논리의 언어는 명제 변수(명제를 넣는 틀)와 논리 연산자(결합자)로 구성된다. 형식 문법에 따라 원자식이나 논리 연산자의 조합으로 표현이나 정식이 귀납적으로 정의된다. 공리 집합은 공집합, 유한 집합, 가산 무한 집합, 또는 공리 도식으로 주어질 수 있다. 의미론에 의해 참 또는 거짓 값을 매기는 해석이 정해지고, 이를 통해 어떤 정식이 정리인지 결정할 수 있다.
2. 1. 문법
집합 가 주어졌을 때, 에 대한 명제 논리의 언어 는 다음과 같은 기호들로 구성된다.- 각 에 대하여, '''원자 명제'''(原子命題, atomic proposition영어)
- '''부정'''(否定, negation영어) 과 '''실질적 함의'''(實質的含意, material implication영어)
- 다른 논리 연산 기호들은 이 두 논리 연산을 통해 나타낼 수 있으므로 사용할 필요가 없다.
- 다른 함수적 완전 집합을 사용하여도 좋다.
명제 논리의 '''논리식'''(論理式, (well-formed) formula영어)은 다음 문법을 따르는 명제 논리 기호들의 문자열이다.
- 모든 원자 명제는 논리식이다.
- 논리식 , 에 대하여, 와 는 논리식이다.
명제 논리는 논리 연결사로 더 이상 분해할 수 없는 지점을 넘어서는 명제의 구조에는 관심이 없으므로, 이러한 ''원자적''(더 이상 나눌 수 없는) 진술을 알파벳 문자로 대체하여 연구하는 것이 일반적이다.[91][1] 이 문자들은 진술을 나타내는 변수, 즉 ''명제 변수''로 해석된다.[1]
명제 논리에서의 ''언어''는 명제 변수(명제를 끼워 넣는 틀)와 논리 연산자(결합자)로 이루어져 있다. 형식 문법에 의해 귀납적으로 그 언어의 표현이나 정식( நன்கு அமைந்த 수식, WFF)이, 원자식이나 문 연산자의 일정한 조합으로 정의된다.
언어의 구성 요소는 다음과 같다.
- 알파벳의 대문자는 명제 변수를 나타낸다. 이들은 원자 논리식이다.
- 다음과 같은 연결사(또는 논리 연산자)를 나타내는 기호: 「¬」(부정), 「∧」(논리곱/연언), 「∨」(논리합/선언), 「→」(논리 함축/함의). ("P → Q"는 "¬P ∨ Q"와 같다는 등으로, 몇몇을 다른 것들의 축약형으로 간주하여 더 적은 연산자(와 기호)로 처리할 수도 있다.)
- 여는 괄호 ( 와 닫는 괄호 )
잘 구성된 수식(WFF)의 집합은 다음 규칙에 따라 귀납적으로 정의된다.
- 기본: 알파벳의 대문자는 잘 구성된 수식이다.
- 귀납 조건 I: 만약 φ가 잘 구성된 수식이라면 ¬φ도 잘 구성된 수식이다.
- 귀납 조건 II: φ와 ψ가 잘 구성된 수식이라면 (φ∧ψ), (φ∨ψ), (φ→ψ)도 잘 구성된 수식이다.
- 폐쇄 조건: 이 외에는 잘 구성된 수식이 아니다.
이것들을 반복적으로 적용함으로써 더 복잡한 잘 구성된 수식을 만들 수 있다. 예를 들어,
- A는 잘 구성된 수식이다.
- ¬A는 잘 구성된 수식이다.
- B는 잘 구성된 수식이다.
- (¬A∨B)는 잘 구성된 수식이다.
2. 2. 공리와 추론 규칙
명제 논리의 추론 규칙과 공리 기본꼴은 다음과 같이 나타낼 수 있다. (임의의 논리식을 나타내는 기호 , , 을 사용한다)- 추론 규칙
- * (전건 긍정의 형식)
:
- 공리 기본꼴
- *
- *
- *
명제 논리는 또 다른 함수적 완전 집합 을 사용하여 전개할 수 있으며, 이 경우 명제 논리의 추론 규칙과 공리 기본꼴은 다음과 같이 나타낼 수 있다. (임의의 논리식을 나타내는 기호 , , 을 사용한다)
- 추론 규칙
- * (선언 도입, disjunction introduction영어, 또는 확장 규칙, expansion rule영어)
:
- * (축소 규칙, contraction rule영어)
:
- * (결합 규칙, associative rule영어)
:
- * (절단 규칙, cut rule영어)
:
- 공리 기본꼴
- * (배중률)
이 절에서는 간단히 하기 위해 공리를 가지지 않거나, 즉 공집합인 공리 집합을 가지는 자연 연역 체계를 사용하기로 한다.
여기서의 명제 논리에서는 여덟 가지 추론 규칙을 고려한다. 이러한 규칙을 통해 참이라고 가정된 식들로부터 다른 참인 식을 도출할 수 있다. 처음 여섯 가지는 단순히 특정한 식을 다른 식으로부터 도출할 수 있다고 기술하고 있다. 반면, 마지막 두 가지 전제에서는 (아직 증명되지 않은) 가정을 일시적으로 사용한다. 이러한 점을 지칭하여 처음 여섯 가지 규칙을 비가정적 규칙, 마지막 두 가지를 가정적 규칙이라고 한다.
- 이중 부정의 제거: 식 ¬¬φ로부터 φ를 추론할 수 있다.
- 합접의 도입: 식 φ와 식 ψ로부터 (φ∧ψ)를 추론할 수 있다.
- 합접의 제거: 식 φ∧ψ로부터 φ와 ψ를 추론할 수 있다.
- 선택의 도입: 식 φ로부터, 어떤 식 ψ에 대해서도 (φ∨ψ)와 (ψ∨φ)를 추론할 수 있다.
- 선택의 제거: (φ∨ψ), (φ→χ), (ψ→χ) 형태의 식으로부터 χ를 추론할 수 있다.
- 전건긍정 (전건긍정식): φ와 (φ→ψ) 형태의 식으로부터 ψ를 추론할 수 있다.
- 조건적 증명: φ를 가정하고 식 ψ가 도출되었다면 (φ→ψ)를 추론할 수 있다.
- 귀류법: φ를 가정하고 ψ와 ¬ψ가 도출되었다면 ¬φ를 추론할 수 있다.
2. 3. 의미론
명제 논리의 모든 논리식의 집합은 로 표기한다. 명제 논리의 '''구조'''는 다음 조건들을 만족시키는 함수 이다.- 모든 논리식 에 대하여:
- (인 경우)
- (인 경우)
- 모든 논리식 , 에 대하여:
- ( 또는 인 경우)
- ( 이고 인 경우)
여기서 와 는 상위 언어의 논리합(OR)과 논리곱(AND) 기호이다.
논리식 와 구조 에 대하여 이 성립한다면, 가 를 '''만족'''시킨다고 하며, 이를 로 표기한다.
명제 논리의 논리식의 집합(즉, 의 부분 집합)을 명제 논리의 '''이론'''이라고 한다. 명제 논리의 이론 와 구조 가 주어졌을 때, 임의의 에 대하여 라면, 가 의 '''모형'''이라고 하며, 이를 로 표기한다. 모형을 갖는 이론을 '''만족 가능 이론'''이라고 한다.
진리값 할당은 명제 변수에 대해 참() 또는 거짓() 값을 대응시키는 함수이다. 진리값 할당은 특정한 서술이 참이 되고 다른 것은 거짓이 되는 '일어날 수 있는 상황'(또는 가능한 세계)에 대한 설명으로 이해할 수 있다.
진리값 할당 가 어떤 경우에 특정한 정식을 만족하는가는 다음 규칙에 따라 정의한다.
- 일 때, 그리고 오직 그 때에만 는 명제 변수 를 만족한다.
- 가 를 만족하지 않을 때, 그리고 오직 그 때에만 는 를 만족한다.
- 가 와 를 만족할 때, 그리고 오직 그 때에만 는 를 만족한다.
- 가 또는 중 적어도 하나를 만족할 때, 그리고 오직 그 때에만 는 를 만족한다.
- 가 를 만족하는데 를 만족하지 않는 경우가 없을 때, 그리고 오직 그 때에만 는 를 만족한다.
3. 성질
명제 논리는 건전성, 완전성, 콤팩트성 정리를 만족시킨다.[119][120] 명제 논리는 개별 명제의 의미보다는 명제들을 논리 연산자로 연결했을 때 어떤 추론이 가능한지를 다룬다. 개별 명제의 의미는 주로 술어 논리에서 다룬다.
일반적으로 명제 논리는 고전 명제 논리를 의미하며[121], 직관주의 논리, 양상 논리, 상관 논리 등 다양한 명제 논리가 존재한다.
명제 논리의 규칙은 다음과 같은 성질을 갖는다.
- 건전성: 어떤 정식의 집합에서 통사적으로 귀결되는 정식은 의미론적으로도 귀결된다.
- 완전성: 어떤 정식의 집합에서 의미론적으로 귀결되는 정식은 통사적으로도 귀결된다.
3. 1. 논리 연산과 함수적 완전 집합
n개의 원자 명제로 구성된 명제 논리의 논리식이 가질 수 있는 진리표는 총 개이다. 특히, 명제 논리는 총 16개의 (서로 동치가 아닌) 2항 논리 연산이 존재하며, 이들은 다음과 같다.[130]모순 명제 | 논리곱 | 비함의 | 역비함의 | 부정 논리합 | 첫째 성분 | 둘째 성분 | 실질적 동치 | ||
---|---|---|---|---|---|---|---|---|---|
1 | 1 | 0 | 1 | 0 | 0 | 0 | 1 | 1 | 1 |
1 | 0 | 0 | 0 | 1 | 0 | 0 | 1 | 0 | 0 |
0 | 1 | 0 | 0 | 0 | 1 | 0 | 0 | 1 | 0 |
0 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 1 |
주어진 명제 논리의 2항 이하의 논리 연산의 집합으로부터 구성된 논리식이 모든 진리표를 나타낼 수 있고, 임의의 한 논리 연산을 제거하였을 때 나타낼 수 없는 진리표가 존재하게 된다면, 이 집합을 '''(극소) 함수적 완전 집합'''이라고 한다. 명제 논리의 극소 함수적 완전 집합은 다음과 같다.[130]
- 크기 1 (총 2개)
- *
- *
- 크기 2 (총 18개)
- *
- *
- *
- *
- *
- *
- *
- *
- *
- *
- *
- *
- *
- *
- *
- *
- *
- *
- 크기 3 (총 6개)
- *
- *
- *
- *
- *
- *
- 크기 4 이상의 극소 함수적 완전 집합은 존재하지 않는다.
4. 역사
명제 논리는 기원전 3세기에 크리시포스가 스토아 논리학이라는 형식 논리로 발전시켰고,[20] 그의 계승자인 스토아 학파가 확장했다. 스토아 논리학은 명제에 초점을 맞춘 반면, 전통적인 삼단논법은 항에 초점을 맞췄다. 그러나 원본 저술 대부분은 분실되었고,[21] 기원후 3세기와 6세기 사이에 스토아 논리학은 잊혀졌다가 20세기에 명제 논리가 다시 발견되면서 부활하였다.[22]
17세기/18세기 수학자 고트프리트 빌헬름 라이프니츠는 기호 논리학을 처음으로 개발했지만, 그의 계산기는 논리학계에 널리 알려지지 않았다. 결과적으로 라이프니츠가 이룬 많은 발전은 조지 불과 어거스터스 드 모르간 같은 논리학자들에 의해 독립적으로 재창조되었다.[23]
고틀로브 프레게의 술어 논리는 명제 논리를 기반으로 하며, "삼단 논리와 명제 논리의 독특한 특징을 결합한 것"으로 묘사된다.[24]
4. 1. 자연 연역, 진리표, 진리표의 발명
게르하르트 겐첸과 스타니스와프 야스코프스키는 자연 연역법을 발명했다.[25] 에버트 빌렘 베스는 진리표를 발명했다.[25] 그러나 진리표 발명에는 여러 인물들의 기여가 있었으며, 그 공헌도는 불확실하다.고틀로브 프레게[26]와 버트런드 러셀[27]의 저술에는 진리표 발명에 영향을 미친 아이디어가 담겨 있다. 실제 표 구조(표로 형식화됨) 자체는 루트비히 비트겐슈타인 또는 에밀 포스트 (또는 둘 다 독립적으로)에게 공을 돌린다.[26] 프레게와 러셀 외에도 필로, 조지 불, 찰스 샌더스 피어스[28], 에른스트 슈뢰더가 진리표에 앞서는 아이디어를 가졌다고 여겨진다. 얀 우카셰비치, 알프레드 노스 화이트헤드, 윌리엄 스탠리 제번스, 존 벤, 클라렌스 어빙 루이스는 표 구조에 공헌했다.[27] 존 쇼스키와 같은 일부 학자들은 "진리표의 '발명가'라는 칭호를 어떤 한 사람에게 부여해야 한다는 것은 분명하지 않다"는 결론을 내렸다.[27]
5. 문장 (Sentences)
명제 논리는 문장의 참/거짓 조건, 또는 어떤 문장이나 문장들의 집합으로부터 문장이 논리적으로 따르는지 여부를 평가할 때, 논리적 귀결의 표준을 명시하는 것으로, 명제 연결사의 의미만을 고려한다.[2] 명제 논리에서 문제가 되는 것은 개별 명제의 의미보다는, 명제를 "그리고", "만약…그러면" 등의 논리 연산자로 연결했을 때 어떤 추론이 가능한가 하는 것이다. 개별 명제의 의미를 주로 다루는 것은 술어 논리 등이다.
명제 논리의 ''언어''는 명제 변수(명제를 끼워 넣는 틀)와 문 연산자(결합자)로 구성된다. 형식 문법에 의해 귀납적으로 그 언어의 표현이나 정식이 정의되며, 공리 도식에 의해 주어질 수도 있다. 의미론에 의해 참 또는 거짓의 값을 매기는 것(또는 해석)이 정해져서 어떤 정식이 옳은지, 즉 정리인지를 결정할 수 있게 된다.
표준적인 명제 논리 외에도, 직관주의 논리적인 명제 논리를 비롯해 양상 논리, 상관 논리 등 다양한 명제 논리가 존재하지만, 보통 명제 논리라고 하면 고전 논리를 가리킨다.[121]
5. 1. 선언문 (Declarative sentences)
명제 논리는 진리값을 갖는 선언문으로 정의된 '''명제'''를 다룬다.[29][1] 명제의 예는 다음과 같다.선언문은 "위키백과는 무엇인가?"와 같은 의문문이나 "이 기사의 주장을 뒷받침하는 인용을 추가해 주세요."와 같은 명령문과 대조된다.[30][31] 이러한 비선언문은 진리값을 갖지 않으며,[32] 비고전 논리인 의문 논리와 명령 논리에서만 다루어진다.
5. 2. 연결사를 사용한 복합 문장 (Compounding sentences with connectives)
명제 논리에서 복합 문장은 더 단순한 문장들로부터 논리 연결사를 사용하여 결합되어 만들어지며, 구성 문장들 간의 관계를 나타낸다.[33][34] 복합 문장의 주요 유형에는 부정, 접속, 선택, 함축, 동치가 있으며,[33] 이는 해당 연결사를 사용하여 명제를 연결하여 형성된다.[35][36] 영어에서 이러한 연결사는 "그리고"(접속), "또는"(선택), "아니다"(부정), "만약"(조건적 함축), 그리고 "만약 그리고 오직 만약"(동치)이라는 단어로 표현된다.[1][13]복합 문장의 예시는 다음과 같다.
- ''위키피디아는 누구나 편집할 수 있는 무료 온라인 백과사전이며, '''그리고''' 수백만 명이 이미 편집하고 있다.'' (접속)
- '''''모든 위키피디아 편집자가 적어도 세 가지 언어를 구사하는 것은 사실이 아니다.''''' (부정)
- '''''런던이 영국의 수도이거나, 또는 런던이 영국의 수도이거나, 혹은 둘 다이다.''''' (선택)
문장에 논리 연결사가 없으면 단순 문장[1] 또는 원자 문장이라고 한다.[34] 하나 이상의 논리 연결사를 포함하면 복합 문장[33] 또는 분자 문장이라고 한다.[34]
문장 연결사는 논리 연결사를 포함하는 더 넓은 범주이다.[2][34] 문장 연결사는 문장을 결합하여 새로운 복합 문장을 만드는 어떠한 언어적 요소이거나,[2][34] 단일 문장을 바꾸어 새로운 문장을 만드는 요소이다.[2] 논리 연결사 또는 명제 연결사는 그것이 작용하는 원래 문장이 명제이거나 명제를 나타낼 때, 그 결과로 생기는 새로운 문장도 명제이거나 명제를 나타내는 특징을 가진 문장 연결사의 한 종류이다.[2] 철학자들은 명제가 정확히 무엇인지에 대해 의견이 다르며,[10][2] 자연어에서 어떤 문장 연결사를 논리 연결사로 간주해야 하는지에 대해서도 의견이 다르다.[34][2] 문장 연결사는 문장 함수라고도 하며,[55] 논리 연결사는 진리 함수라고도 한다.[55]
6. 논증 (Arguments)
논증은 '''전제'''라고 불리는 문장들의 집합과 '''결론'''이라고 불리는 하나의 문장, 이 두 가지 요소로 정의된다.[37][34][55] 전제는 결론을 ''뒷받침하는 것''으로, 결론은 전제로부터 ''추론되는 것''으로 주장된다.[34][55]
명제 논리에서의 논증 예시는 예시 논증 하위 섹션에서 확인할 수 있다.
6. 1. 예시 논증 (Example argument)
'''전제 1:''' 비가 온다면, 구름이 낀다.'''전제 2:''' 비가 온다.
'''결론:''' 구름이 낀다.
이 논증의 논리적 형식은 모두스 포넨스[91]로 알려져 있으며, 이는 고전 논리에서 타당한 형식이다.[38] 따라서 고전 논리에서 이 논증은 ''타당''하지만, 주어진 문맥에서의 기상학적 사실에 따라 ''건전''할 수도 있고 아닐 수도 있다.
6. 2. 타당성과 건전성 (Validity and soundness)
어떤 논증이 '''타당하다'''는 것은, 그 전제들이 모두 참이라면 결론이 참이어야 한다는 것이 ''필요조건''임을 의미한다.[37][39][40] 다른 말로, 논증이 타당하다는 것은 전제들이 모두 참인데 결론이 거짓인 경우가 ''불가능하다''는 것을 의미한다.[40][37]타당성은 ''건전성''과 대조된다.[40] 어떤 논증이 '''건전하다'''는 것은, 그 논증이 타당하고 모든 전제가 참이라는 것을 의미한다.[37][40] 그렇지 않으면 ''비건전적''이다.[40]
일반적으로 논리학은 타당한 논증을 정확하게 규정하는 것을 목표로 한다.[34] 이는 결론이 전제들의 논리적 귀결인 논증을 타당한 논증으로 정의함으로써 이루어지는데,[34] 이것을 ''의미론적 귀결''로 이해할 때는, 전제가 참인데 결론은 참이 아닌 ''경우''가 없다는 것을 의미한다.[34]
7. 형식화 (Formalization)
명제 논리는 공식 체계를 통해 연구되며, 여기서 공식은 형식 언어의 해석을 통해 명제를 나타낸다. 이 형식 언어는 증명 체계의 기반이 되며, 이를 통해 전제로부터 결론을 도출할 수 있다.[119][120]
명제 논리에서 중요한 것은 개별 명제의 의미보다는, 명제들을 "그리고", "만약...그러면" 등의 논리 연산자로 연결했을 때 어떤 추론이 가능한가 하는 것이다. 개별 명제의 의미를 다루는 것은 술어 논리 등이다.[121]
일반적으로 명제 논리라고 하면 고전 명제 논리를 의미한다. 명제 계산은 "문법적으로 괜찮은" 정식(well-formed formula)의 집합, 공리의 집합, 그리고 변형 규칙의 집합으로 이루어진 형식적 체계이다.
각각의 표현이 수학적 표현으로 해석될 때, 표현의 변형 규칙은 의미 동등성을 유지하도록 주어진다. 표현이 논리 체계 자체로 해석될 때에는 "의미 동등성"이 논리적 동등성을 가리키도록 변형 규칙이 주어져, 주어진 표현으로부터 논리적으로 동등한 표현을 도출할 수 있다.
명제 논리에서의 ''언어''는 명제 변수와 문 연산자(결합자)로 이루어져 있다. 형식 문법에 의해 그 언어의 표현이나 정식이, 원자식이나 문 연산자의 조합으로 정의된다. 공리의 집합은 공집합, 유한 집합, 가산 무한 집합이거나, 공리 도식에 의해 주어질 수 있다. 의미론에 의해 참 또는 거짓의 값 매김(또는 해석)이 정해져서 어떤 정식이 정리인지를 결정할 수 있다.
표준적인 명제 논리 외에도, 언어를 구성하는 연산자나 변수가 다르거나, 공리나 추론 규칙이 다른 다양한 방법들이 존재한다.
7. 1. 명제 변수 (Propositional variables)
명제 논리에서는 더 이상 분해할 수 없는 원자적 진술을 알파벳 문자로 대체하여 연구하는 것이 일반적이다.[91][1] 이러한 문자들은 진술을 나타내는 변수, 즉 '''명제 변수'''로 해석된다.[1] 예를 들어, 명제 변수를 사용하면 다음과 같은 예시 논증을 기호화할 수 있다.- '''전제 1:'''
- '''전제 2:'''
- '''결론:'''
여기서 를 "비가 온다"로, 를 "흐리다"로 해석하면, 이 기호 표현은 자연어로 된 원래 표현과 정확히 일치한다. 또한, 같은 논리 형식을 가진 다른 추론에도 일치하게 된다.
공식 체계를 사용하여 형식 논리를 나타낼 때는 진술 문자(일반적으로 , , 과 같은 대문자 로마 문자)만 직접 표현된다. 해석될 때 나타나는 자연어 명제는 체계의 범위를 벗어나며, 공식 체계와 해석 간의 관계 또한 공식 체계 자체의 범위를 벗어난다.
7. 2. 겐첸 표기법 (Gentzen notation)
겐첸의 자연 연역과 시퀀트 계산 표기법은 전제들을 추론선 위에 표시하고, 결론을 추론선 아래에 적는 방식이다.[41][15] 쉼표는 전제들의 결합을 의미한다.[42]예를 들어, 모두스 포넨스의 타당성이 공리로 받아들여졌을 때, 다음과 같이 표현할 수 있다.
:
이때 추론선은 '구문적 귀결'을 나타내며,[15] '연역적 귀결'이라고도 한다.[43] 구문적 귀결은 ⊢ 기호로 표현할 수 있다.[44][43] 따라서 위의 식은 로 쓸 수 있다.
구문적 귀결은 '의미론적 귀결'과 대조된다.[45] 의미론적 귀결은 ⊧ 기호로 표현된다.[44][43] 위 예시에서 결론은 자연 연역의 추론 규칙인 모두스 포넨스가 가정되었기 때문에 구문적으로 따른다.
8. 언어 (Language)
명제 논리의 언어는 명제 변수와 논리 연산자로 구성된다. 명제 변수는 명제를 나타내는 기호이고, 논리 연산자는 명제들을 연결하여 새로운 명제를 만드는 기호이다.
명제 논리의 언어는 다음과 같은 요소들로 구성된다.
- 알파벳 대문자: 명제 변수를 나타내며, 원자 논리식이라고도 한다. 예를 들어, 'P', 'Q', 'R' 등이 있다.
- 연결사 (논리 연산자):
- `¬`: 부정 (negation)
- `∧`: 논리곱/연언 (conjunction)
- `∨`: 논리합/선언 (disjunction)
- `→`: 논리 함축/함의 (implication)
- 괄호: `(`, `)`
이 요소들을 조합하여 복잡한 논리식을 만들 수 있다. 예를 들어, "P → Q"는 "P이면 Q이다"라는 의미를 나타낸다.
논리식(well-formed formula)은 다음 규칙에 따라 귀납적으로 정의된다.
- 기본: 알파벳 대문자는 논리식이다.
- 귀납 조건 I: φ가 논리식이면, ¬φ도 논리식이다.
- 귀납 조건 II: φ와 ψ가 논리식이면, (φ∧ψ), (φ∨ψ), (φ→ψ)도 논리식이다.
- 폐쇄 조건: 이 외에는 논리식이 아니다.
예를 들어:
명제 논리는 형식 언어의 해석을 통해 명제를 나타내며, 명제 변수를 사용하여 문장을 기호화한다.
8. 1. 구문 (Syntax)
집합 가 주어졌을 때, 에 대한 명제 논리의 언어 는 다음과 같은 기호들로 구성된다.- 각 에 대하여, '''원자 명제'''(原子命題, atomic proposition영어)
- '''부정'''(否定, negation영어) 과 '''실질적 함의'''(實質的含意, material implication영어)
다른 논리 연산 기호들은 이 두 논리 연산을 통해 나타낼 수 있으므로 사용할 필요가 없다. 다른 함수적 완전 집합을 사용하여도 좋다.
명제 논리의 '''논리식'''(論理式, (well-formed) formula영어)은 다음 문법을 따르는 명제 논리 기호들의 문자열이다.
- 모든 원자 명제는 논리식이다.
- 논리식 , 에 대하여, 와 는 논리식이다.
주어진 논리 체계의 '''문장'''(文章, sentence영어)은 자유 변수를 갖지 않는 논리식으로 정의된다. 명제 논리의 논리식은 변수를 포함하지 않으므로 모든 논리식은 문장이다.
명제 논리는 일반적으로 공식 체계를 통해 연구되는데, 여기서 공식은 형식 언어의 해석을 통해 명제를 나타낸다.
명제 변수를 사용하면 다음과 같이 기호화된다.
:\'''전제 1:'''
:\'''전제 2:'''
:\'''결론:'''
를 "비가 온다"로, 를 "흐리다"로 해석하면 이러한 기호 표현은 자연어로 된 원래 표현과 정확히 일치한다. 뿐만 아니라, 같은 논리 형식을 가진 다른 추론에도 일치하게 된다.
명제 논리의 언어 ()는[43][46][34] 다음과 같은 용어로 정의된다.[2][14]
1. 원시 기호 집합으로, ''원자 공식'', ''원자 문장'',[91][34] ''원자'',[47] ''자리 표시자'', ''기본 공식'',[47] ''명제 문자'', ''문장 문자'',[91] 또는 ''변수''라고 한다.
2. 연산자 기호 집합으로, ''접속사'',[18][1][49] ''논리 접속사'',[1] ''논리 연산자'',[1] ''진리 함수적 접속사'',[1] ''진리 함수'',[55] 또는 ''명제 접속사''라고 한다.[2]
''잘 형성된 공식''은 원자 공식이거나, 문법 규칙에 따라 연산자 기호를 사용하여 원자 공식으로부터 구성될 수 있는 공식이다.
원자 명제 변수 집합 , , , ... 와 명제 연결사 집합 , , , ..., , , , ..., , , , ...가 주어졌을 때, 명제 논리의 공식은 다음 정의에 따라 재귀적으로 정의된다.[2][14][49]
:\'''정의 1''': 원자 명제 변수는 공식이다.
:\'''정의 2''': 이 명제 연결사이고, A, B, C, …가 m개의, 원자일 수도 있고 아닐 수도 있으며, 구별될 수도 있고 아닐 수도 있는 공식의 수열이면, 을 A, B, C, …에 적용한 결과는 공식이다.
:\'''정의 3''': 그 외에는 공식이 아니다.
을 A, B, C, …에 적용한 결과를 함수 표기법으로 (A, B, C, …)으로 쓴다면, 다음은 잘 형성된 공식의 예이다.
위에서 ''정의 2''로 제시된 공식의 구성을 담당하는 부분은 콜린 호손에 의해 ''구성 원리''라고 불린다.[91]
위에서 ''정의 3''으로 제시된 "그 외에는 공식이 아니다"라는 정의는 구문의 다른 정의에 의해 특별히 요구되지 않는 공식을 언어에서 제외한다.[55]
위에 제시된 구문 정의의 대안으로 언어 에 대한 맥락 자유(CF) 문법을 배커스-나우어 형식(BNF)으로 작성하는 방법이 있다.[51][52] 여러 가지 방법으로 작성할 수 있는데,[51] 일반적인 다섯 가지 연결사에 대한 특히 간결한 방법은 다음과 같은 단일 절이다.[52][53]
:
명제 논리에서의 ''언어''는 명제 변수(명제를 끼워 넣는 틀)와 연산자(결합자)로 이루어져 있다.
언어의 구성 요소는 다음과 같다.
- 알파벳의 대문자는 명제 변수를 나타낸다. 이들은 원자 논리식이다.
- 다음과 같은 연결사(또는 논리 연산자)를 나타내는 기호: 「¬」(부정), 「∧」(논리곱/연언), 「∨」(논리합/선언), 「→」(논리 함축/함의).
- 여는 괄호 ( 와 닫는 괄호 )
잘 구성된 수식의 집합은 다음 규칙에 따라 귀납적으로 정의된다.
- 기본: 알파벳의 대문자는 잘 구성된 수식이다.
- 귀납 조건 I: 만약 φ가 잘 구성된 수식이라면 ¬φ도 잘 구성된 수식이다.
- 귀납 조건 II: φ와 ψ가 잘 구성된 수식이라면 (φ∧ψ), (φ∨ψ), (φ→ψ)도 잘 구성된 수식이다.
- 폐쇄 조건: 그 외에는 잘 구성된 수식이 아니다.
이것들을 반복적으로 적용함으로써 더 복잡한 잘 구성된 수식을 만들 수 있다. 예를 들어,
- A는 잘 구성된 수식이다.
- ¬A는 잘 구성된 수식이다.
- B는 잘 구성된 수식이다.
- (¬A∨B)는 잘 구성된 수식이다.
8. 2. 상수와 도식 (Constants and schemata)
수학자들은 때때로 명제 상수(명제 변수)와 스키마를 구분한다. '명제 상수'는 특정 명제를 나타내는 반면,[54] '명제 변수'는 모든 원자 명제의 집합을 범위로 한다.[54] 그러나 스키마 또는 '스키마 문자'는 모든 공식을 범위로 한다.[55][1] (스키마 문자는 '메타변수'라고도 한다.)[37] 명제 상수는 일반적으로 A, B, C로, 명제 변수는 P, Q, R로, 그리고 스키마 문자는 그리스 문자, 가장 자주 φ, ψ, χ로 나타낸다.[55][1]일부 저자들은 형식 시스템에서 "참"(항상 참으로 평가됨)이라고 불리는 특수 기호 과 "거짓"(항상 거짓으로 평가됨)이라고 불리는 특수 기호 의 두 가지 "명제 상수"만을 인식한다.[56][57][58] 다른 저자들은 같은 의미를 가진 이러한 기호들을 포함하지만, "0항 진리 함수"[55] 또는 동등하게 "영항 연결자"로 간주한다.[49]
9. 의미론 (Semantics)
명제 논리에서 모든 논리식의 집합은 로 표기한다. 명제 논리의 '''구조'''는 다음 조건들을 만족시키는 함수 이다.
- 모든 논리식 에 대하여,
:
- 모든 논리식 , 에 대하여,
:
(여기서 , 는 메타 언어의 논리합·논리곱 기호이다.)
논리식 와 구조 에 대하여 이 성립한다면, 가 를 '''만족'''시킨다고 하며, 이를 로 표기한다.
명제 논리의 논리식의 집합(즉, 의 부분 집합)을 명제 논리의 '''이론'''이라고 한다. 명제 논리의 이론 와 구조 가 주어졌을 때, 임의의 에 대하여 라면, 가 의 '''모형'''이라고 하며, 이를 로 표기한다. 모형을 갖는 이론을 '''만족 가능 이론'''이라고 한다.
명제 논리는 일반적으로 공식 체계를 통해 연구되는데, 여기서 공식은 형식 언어의 해석을 통해 명제를 나타낸다. 이 형식 언어는 증명 체계의 기반이 되며, 이를 통해 결론이 전제의 논리적 귀결인 경우에만 전제로부터 결론을 도출할 수 있다.
명제 논리에서 중요한 것은 개별 명제의 의미보다는, 명제들을 "그리고", "만약…그러면" 등의 논리 연산자로 연결했을 때 어떤 추론이 가능한가 하는 것이다. 개별 명제의 의미를 주로 다루는 것은 술어 논리 등이다.
추론의 성질에 따라 직관주의 논리적인 명제 논리, 양상 논리, 상관 논리 등 다양한 명제 논리가 있지만, 보통 명제 논리라고 하면 고전 명제 논리를 가리킨다.
일반적으로 명제 계산은 "문법적으로 괜찮은" 통어적인 표현(정식의 집합), 그 표현의 일부로 이루어지는 부분집합(공리의 집합), 표현의 공간 위에 이항 관계를 정의하는 변형 규칙의 집합으로 이루어지는 형식적 체계이다.
보통 각 표현이 수학적 표현으로 구체적으로 해석될 때, 표현의 변형 규칙이 일정한 의미 동등성을 유지하도록 주어진다. 특히 표현이 논리 체계 자체로 해석될 때는 "의미 동등성"이 논리적 동등성을 가리키도록 변형 규칙이 주어진다. 이러한 변형 규칙에 의해 주어진 표현으로부터 논리적으로 동등한 표현을 도출할 수 있다.
명제 논리에서의 ''언어''는 명제 변수(명제를 끼워 넣는 틀)와 논리 연산자(결합자)로 이루어져 있다. 형식 문법에 의해 귀납적으로 그 언어의 표현이나 정식이, 원자식이나 문 연산자의 일정한 조합으로 정의된다. 공리의 집합은 공집합, 유한 집합, 가산 무한 집합일 수 있으며, 공리 도식으로 주어질 수도 있다. 의미론에 의해 참 또는 거짓의 값 매김(또는 해석)이 정해지며, 이를 통해 어떤 정식이 옳은지, 즉 정리인지를 결정할 수 있다.
진리값 할당은 명제 변수에 대해 '''참'''() 또는 '''거짓'''() 값을 대응시키는 함수이다. 비형식적으로, 진리값 할당은 특정한 서술이 참이 되고 다른 것은 거짓이 되는 '일어날 수 있는 상황'(또는 가능한 세계)에 대한 설명으로 이해할 수 있다.
진리값 할당 가 어떤 경우에 특정한 정식을 만족하는가는 다음 규칙에 따라 정의한다.
- 일 때, 그리고 오직 그 때에만 는 명제 변수 를 만족한다.
- 가 를 만족하지 않을 때, 그리고 오직 그 때에만 는 를 만족한다.
- 가 와 를 만족할 때, 그리고 오직 그 때에만 는 를 만족한다.
- 가 또는 중 적어도 하나를 만족할 때, 그리고 오직 그 때에만 는 를 만족한다.
- 가 를 만족하는데 를 만족하지 않는 경우가 없을 때, 그리고 오직 그 때에만 는 를 만족한다.
이 정의에 의해 식 가 특정한 식의 집합 에서 따른다는 것이 무엇을 의미하는지 공식화할 수 있다. 비격식적으로 말하면, 이것은 의 식이 성립하는 모든 세계에서 가 성립한다는 것을 의미한다. 이것은 다음과 같이 형식화할 수 있다: 의 모든 식을 만족하는 진리값 할당이 반드시 를 만족할 때, 정식 는 에서 의미론적으로 귀결된다(또는 도출된다).
마지막으로, 통사적인 귀결이라는 관계를, 가 위에 제시된 추론 규칙에 따라 유한한 단계에서 의 식으로부터 도출될 때, 그리고 오직 그 때에만 는 에서 통사적으로 귀결된다고 정의한다. 이에 따라 추론 규칙 집합의 건전성과 완전성을 공식화할 수 있다.
- '''건전성''': 만약 가 정식의 집합 에서 통사적으로 귀결된다면 는 에서 의미론적으로 귀결된다.
- '''완전성''': 만약 가 에서 의미론적으로 귀결된다면 는 에서 통사적으로 귀결된다.
9. 1. 해석 (경우)과 논증 (Interpretation (case) and argument)
주어진 언어 에 대해, '''해석''',[63] '''값 매김''',[48] 또는 '''경우'''[34]는 의 각 공식에 대한 의미 값의 대입이다.[34] 고전 논리의 형식 언어의 경우, 경우는 의 각 공식에 대해 진리값인 참('''T''', 또는 1)과 거짓('''F''', 또는 0) 중 하나를 대입하는 것으로 정의된다(둘 다는 아님).[64][65] 고전 논리의 규칙을 따르는 해석은 때때로 '''부울 값 매김'''이라고 한다.[48][66] 고전 논리에 대한 형식 언어의 해석은 종종 진리표를 통해 표현된다.[67][1] 각 공식에 단일 진리값만 할당되므로, 해석은 정의역이 이고 공역이 의미 값 집합 ,[2] 또는 인 함수로 볼 수 있다.[34]개의 서로 다른 명제 기호에 대해 개의 서로 다른 가능한 해석이 있다. 예를 들어, 특정 기호 의 경우, 개의 가능한 해석이 있다. 즉, 에 '''T'''가 할당되거나 '''F'''가 할당된다. 쌍 , 의 경우에는 개의 가능한 해석이 있다. 즉, 둘 다 '''T'''가 할당되거나, 둘 다 '''F'''가 할당되거나, 에는 '''T'''가 할당되고 에는 '''F'''가 할당되거나, 에는 '''F'''가 할당되고 에는 '''T'''가 할당된다.[67] 이 , 즉 가산 가능한 많은 명제 기호를 가지므로, 개, 따라서 비가산 가능한 많은 서로 다른 가능한 의 해석이 있다.[67]
가 해석이고 와 가 공식을 나타내는 경우, 논증의 정의는 쌍으로 나타낼 수 있다. 여기서 은 전제 집합이고 는 결론이다. 논증의 ''타당성'', 즉 인 성질은 '''반례'''가 없다는 것으로 나타낼 수 있다. 여기서 '''반례'''는 논증의 전제 가 모두 참이지만 결론 가 참이 아닌 경우 로 정의된다.[34][91] 이것은 결론이 전제의 ''의미론적 귀결''이라고 말하는 것과 같다.
9. 2. 명제 연결사의 의미론 (Propositional connective semantics)
논리 연결사는 적용되는 명제 변수가 두 가지 가능한 진릿값 중 하나를 취할 때 취하는 진릿값만으로 의미적으로 정의된다.[1][34] 논리 연결사는 이를 사용하여 원자로 형성된 문장의 진리값이 적용되는 원자의 진리값에만 의존하도록 정의된다.[63][34] 이러한 가정은 콜린 하우슨에 의해 진릿값 함수성 ''연결사''의 가정으로 언급된다.[91]9. 2. 1. 진리표를 통한 의미론 (Semantics via truth tables)
논리연결사는 적용되는 명제 변수가 두 가지 가능한 진릿값 중 하나를 취할 때 취하는 진릿값만으로 의미적으로 정의된다.[1][34] 연결사의 의미적 정의는 일반적으로 아래와 같이 각 연결사에 대한 진리표로 표현된다.[1][34][102]p | q | p ∧ q | p ∨ q | p → q | p ↔ q | ¬p | ¬q |
---|---|---|---|---|---|---|---|
T | T | T | T | T | T | F | F |
T | F | F | T | F | F | F | T |
F | T | F | T | T | F | T | F |
F | F | F | F | T | T | T | T |
이 표는 주요 다섯 가지 논리연결사[13][14][15][16]인 논리곱(여기서는 p ∧ q로 표기), 논리합(p ∨ q), 조건문(p → q), 논리적 동치(p ↔ q) 및 부정(¬p 또는 ¬q)을 다룬다. 이것은 이러한 연산자 각각의 의미론을 결정하기에 충분하다.[1][68][34] 더 다양한 종류의 연결사에 대한 더 많은 진리표는 진리표 문서를 참조하면 된다.
진리표는 모든 가능한 시나리오에서 명제 논리 표현의 참값을 결정하는 데 사용되는 의미론적 증명 방법이다.[87] 구성 원자의 참값을 모두 나열함으로써, 진리표는 명제가 참인지, 거짓인지, 항진인지, 또는 모순인지를 보여줄 수 있다.[88]
9. 2. 2. 할당 표현을 통한 의미론 (Semantics via assignment expressions)
일부 저자들은 명제 목록을 사용하여 연결사의 의미론을 기술한다. 이 형식에서 φ의 해석을 라 할 때, 다섯 가지 주요 논리연결사는 다음과 같이 정의된다.[55][48]- 는, 와 동치이다.
- 는, 이고 와 동치이다.
- 는, 이거나 와 동치이다.
- 는, 이면 임이 참인 것과 동치이다.
- 는, 인 것과 인 것이 동치인 것과 동치이다.
대신 φ의 해석을 로 나타낼 수도 있고,[55][69] 위의 정의에서 를 간단히 "φ는 값 를 갖는다"라는 문장으로 쓸 수도 있다.[48]
일부 논리 연결사는 다른 연결사로 정의될 수 있다. 예를 들어, 함축(p → q)은 부정과 논리합을 이용하여 ¬p ∨ q로 정의될 수 있으며,[72] 논리합은 부정과 논리곱을 이용하여 ¬(¬p ∧ ¬q)로 정의될 수 있다.[48] 사실, 모든 고전적 명제 논리의 항진 명제만이 정리인 진리함수적으로 완전한 시스템은 논리합과 부정만을 사용하여 도출될 수 있다.
9. 3. 의미론적 참, 타당성, 귀결 (Semantic truth, validity, consequence)
주어진 언어 에 대해, '''해석''',[63] '''값 매김''',[48] 또는 '''경우'''[34]는 의 각 공식에 대한 의미 값의 대입이다.[34] 고전 논리의 형식 언어의 경우, 경우는 의 각 공식에 대해 진리값인 참('''T''', 또는 1)과 거짓('''F''', 또는 0) 중 하나를, 하지만 둘 다 아닌 것을 대입하는 것으로 정의된다.[64][65] 고전 논리의 규칙을 따르는 해석은 때때로 '''부울 값 매김'''이라고 한다.[48][66] 고전 논리에 대한 형식 언어의 해석은 종종 진리표를 통해 표현된다.[67][1] 각 공식에 단일 진리값만 할당되므로, 해석은 정의역이 이고 공역이 의미 값 집합 ,[2] 또는 인 함수로 볼 수 있다.[34]개의 서로 다른 명제 기호에 대해 개의 서로 다른 가능한 해석이 있다. 예를 들어, 특정 기호 의 경우, 개의 가능한 해석이 있다. 즉, 에 '''T'''가 할당되거나 '''F'''가 할당된다. 그리고 쌍 , 의 경우, 개의 가능한 해석이 있다.[67] 이 , 즉 가산 가능한 많은 명제 기호를 가지므로, 개, 따라서 비가산 가능한 많은 서로 다른 가능한 의 해석이 있다.[67]
와 를 언어 의 공식(또는 문장)으로, 를 의 해석(또는 경우)으로 하면, 다음과 같은 정의가 적용된다.[67][65]
- '''경우에서의 참''':[34] 의 문장 는 해석 하에서 참(참값 '''T''')이면 참이다.[65][67] 가 하에서 참이라면, 를 의 '''모델'''이라고 한다.[67]
- '''경우에서의 거짓''':[34] 가 해석 하에서 거짓인 것은, 가 하에서 참일 때이며, 그때만 그렇다.[67][80][34] 이것은 경우에서의 거짓에 대한 "부정의 참" 정의이다. 경우에서의 거짓은 "여집합" 정의에 의해서도 정의될 수 있다. 즉, 가 해석 하에서 거짓인 것은, 가 하에서 참이 아닐 때이며, 그때만 그렇다.[65][67] 고전 논리에서는 이러한 정의들이 동치이지만, 비고전 논리에서는 그렇지 않다.[34]
- '''의미론적 귀결''': 의 문장 가 문장 의 '''의미론적 귀결'''()인 것은, 가 참이고 가 참이 아닌 해석이 없을 때이다.[65][67][34]
- '''타당한 공식(항진명제)''': 의 문장 가 '''논리적으로 타당'''()하거나 '''항진명제'''[76][77][48]인 것은, 모든 해석 하에서 참이거나, '''모든 경우에서 참'''일 때이다.[65][67]
- '''모순이 없는 문장''': 의 문장이 '''모순이 없다'''는 것은 적어도 하나의 해석 하에서 참일 때이다. 모순이 없지 않다면 '''모순된다'''고 한다.[65][67] 모순된 공식은 '''자기 모순적'''[1]이라고도 하며, '''자기 모순'''[1] 또는 단순히 '''모순'''[97][98][99]이라고 한다. 비록 후자의 이름은 때때로 형태의 명제에만 특별히 사용되기도 한다.[1]
의 해석(경우) 에 대해, 다음과 같은 정의가 때때로 주어 진다.
- '''완전한 경우''': 경우 가 '''완전한''' 것은, 의 어떤 에 대해서도 가 에서 참이거나 가 에서 참일 때이며, 그때만 그렇다.[34][78]
- '''모순이 없는 경우''': 경우 가 '''모순이 없는''' 것은, 와 가 모두 에서 참인 의 가 없을 때이며, 그때만 그렇다.[34][79]
모든 경우가 완전하고 모순이 없다고 가정하는 고전 논리[34]에 대해서는 다음 정리가 적용된다.
- 주어진 해석에 대해, 주어진 공식은 그 해석 하에서 참이거나 거짓이다.[67][80]
- 어떤 공식도 같은 해석 하에서 참이면서 동시에 거짓일 수 없다.[67][80]
- 가 하에서 참인 것은, 가 하에서 거짓일 때이며, 그때만 그렇다;[67][80] 가 하에서 참인 것은, 가 하에서 참이 아닐 때이며, 그때만 그렇다.[67]
- 와 가 모두 하에서 참이라면, 는 하에서 참이다.[67][80]
- 이고 라면, 이다.[67]
- 가 하에서 참인 것은, 가 하에서 참이 아니거나 가 하에서 참일 때이며, 그때만 그렇다.[67]
- 인 것은, 가 논리적으로 타당할 때이며, 즉 인 것은 일 때이며, 그때만 그렇다.[67][80]
10. 증명 체계 (Proof systems)
명제 논리의 증명 체계는 크게 의미론적 증명 체계와 구문론적 증명 체계로 나뉜다.
의미론적 증명 체계는 진리값을 이용하여 명제의 참, 거짓을 판별하는 방식이다. 주어진 명제 논리 언어 의 각 공식에 참(T 또는 1) 또는 거짓(F 또는 0) 값을 대입하는 해석을 통해 증명이 이루어진다.[63][48][34] 이러한 해석은 진리표를 통해 표현할 수 있다.[67][1] 예를 들어, 개의 명제 기호에 대해서는 개의 가능한 해석이 존재한다.[67] 어떤 논증이 타당하다는 것은 전제가 모두 참이지만 결론은 거짓인 반례가 없음을 의미하며, 이는 결론이 전제의 의미적 귀결이라는 것과 같다.[34][91]
구문론적 증명 체계는 공식 체계를 통해 명제를 도출하는 방식이다. 공식은 형식 언어의 해석을 통해 명제를 나타내며, 증명 체계는 전제로부터 결론을 도출하는 규칙을 제공한다. 명제 논리는 논리식들 간의 관계를 나타내는 데 사용되며, 변형 규칙을 이용한 "증명" 또는 "전개" 절차를 통해 논리적 관계를 밝힌다. 증명은 번호가 매겨진 여러 줄의 서술로 표현되며, 각 줄은 근거와 함께 해당 논리식을 도출하는 과정을 보여준다. 증명에 필요한 가정은 "전제"로 명시하고 결론은 마지막 줄에 제시한다. 모든 줄의 내용이 이전 줄의 내용을 바탕으로 변형 규칙을 정확하게 적용하여 얻어진 것이면 증명이 완료된 것으로 간주한다.
명제 논리에서는 전건 긍정과 같은 추론 규칙과 공리 기본꼴을 사용한다. 명제 논리는 또 다른 함수적 완전 집합 을 사용하여 전개할 수도 있으며, 이 경우 배중률과 같은 공리 기본꼴을 사용한다.
10. 1. 의미론적 증명 체계 (Semantic proof systems)
해석은 주어진 언어 의 각 공식에 의미 값을 대입하는 것이다.[63][48][34] 이는 진리값인 참(T 또는 1)과 거짓(F 또는 0) 중 하나를 각 공식에 할당하는 방식으로 정의된다.[64][65] 이러한 해석은 진리표를 통해 표현될 수 있다.[67][1]개의 명제 기호에 대해 개의 가능한 해석이 존재한다. 예를 들어, 명제 기호 는 T 또는 F의 두 가지 해석이 가능하며, 와 두 기호에 대해서는 네 가지 해석이 가능하다.[67]
논증의 타당성은 반례, 즉 전제가 모두 참이지만 결론이 거짓인 경우가 없는 것으로 나타낼 수 있다.[34][91] 이는 결론이 전제의 의미적 귀결이라는 것과 같다.
의미 표는 명제의 진릿값을 체계적으로 탐색하는 의미론적 증명 기법이다.[89] 이 방법은 각 가지가 가능한 해석을 나타내는 트리를 구성하며, 모든 가지가 모순이면 원래 명제는 모순이고 그 부정은 항진명제가 된다.[90][91]
10. 1. 1. 진리표 (Truth tables)
주어진 언어 에 대해, 해석,[63] 값 매김,[48] 또는 경우[34]는 의 각 공식에 대한 의미 값의 대입이다.[34] 고전 논리의 형식 언어의 경우, 경우는 의 각 공식에 대해 진리값인 참('''T''', 또는 1)과 거짓('''F''', 또는 0) 중 하나를, 하지만 둘 다 아닌 것을 대입하는 것으로 정의된다.[64][65] 고전 논리의 규칙을 따르는 해석은 때때로 부울 값 매김이라고도 한다.[48][66] 고전 논리에 대한 형식 언어의 해석은 종종 진리표를 통해 표현된다.[67][1] 각 공식에 단일 진리값만 할당되므로, 해석은 정의역이 이고 공역이 의미 값 집합 ,[2] 또는 인 함수로 볼 수 있다.[34]개의 서로 다른 명제 기호에 대해 개의 서로 다른 가능한 해석이 있다. 예를 들어, 특정 기호 의 경우, 개의 가능한 해석이 있는데, 즉 에 '''T'''가 할당되거나 '''F'''가 할당되는 경우이다. 그리고 쌍 , 의 경우, 개의 가능한 해석이 있는데, 즉 둘 다 '''T'''가 할당되거나, 둘 다 '''F'''가 할당되거나, 에는 '''T'''가 할당되고 에는 '''F'''가 할당되거나, 에는 '''F'''가 할당되고 에는 '''T'''가 할당되는 경우이다.[67] 이 , 즉 가산 가능한 많은 명제 기호를 가지므로, 개, 따라서 비가산 가능한 많은 서로 다른 가능한 의 해석이 있다.[67]
논리연결사는 적용되는 명제 변수가 두 가지 가능한 진릿값 중 하나를 취할 때 취하는 진릿값만으로 의미적으로 정의되기 때문에,[1][34] 연결사의 의미적 정의는 일반적으로 아래와 같이 각 연결사에 대한 진리표로 표현된다.[1][34][102]
p | q | p ∧ q | p ∨ q | p → q | p ↔ q | ¬p | ¬q |
---|---|---|---|---|---|---|---|
T | T | T | T | T | T | F | F |
T | F | F | T | F | F | F | T |
F | T | F | T | T | F | T | F |
F | F | F | F | T | T | T | T |
이 표는 주요 다섯 가지 논리연결사[13][14][15][16], 즉 논리곱(여기서는 p ∧ q로 표기), 논리합(p ∨ q), 조건문(p → q), 논리적 동치(p ↔ q) 및 부정(¬p 또는 ¬q)를 다룬다. 이것은 이러한 연산자 각각의 의미론을 결정하기에 충분하다.[1][68][34]
10. 1. 2. 의미 표 (Semantic tableaux)
주어진 언어 에 대해, '''해석''',[63] '''값 매김''',[48] 또는 '''경우'''[34]는 의 각 공식에 대한 의미 값의 대입이다.[34] 고전 논리의 형식 언어의 경우, 경우는 의 각 공식에 대해 진리값인 참('''T''', 또는 1)과 거짓('''F''', 또는 0) 중 하나를, 하지만 둘 다 아닌 것을 대입하는 것으로 정의된다.[64][65] 고전 논리의 규칙을 따르는 해석은 때때로 '''부울 값 매김'''이라고 한다.[48][66] 고전 논리에 대한 형식 언어의 해석은 종종 진리표를 통해 표현된다.[67][1] 각 공식에 단일 진리값만 할당되므로, 해석은 정의역이 이고 공역이 의미 값 집합 ,[2] 또는 인 함수로 볼 수 있다.[34]개의 서로 다른 명제 기호에 대해 개의 서로 다른 가능한 해석이 있다. 예를 들어, 특정 기호 의 경우, 개의 가능한 해석이 있는데, 에 '''T'''가 할당되거나 '''F'''가 할당되는 경우이다. 쌍 , 의 경우에는 개의 가능한 해석이 있는데, 둘 다 '''T'''가 할당되거나, 둘 다 '''F'''가 할당되거나, 에는 '''T'''가 할당되고 에는 '''F'''가 할당되거나, 에는 '''F'''가 할당되고 에는 '''T'''가 할당되는 경우이다.[67] 이 , 즉 가산 가능한 많은 명제 기호를 가지므로, 개, 따라서 비가산 가능한 많은 서로 다른 가능한 의 해석이 있다.[67]
가 해석이고 와 가 공식을 나타내는 경우, 논증의 ''타당성'', 즉 인 성질은 '''반례'''가 없다는 것으로 나타낼 수 있다. 여기서 '''반례'''는 논증의 전제 가 모두 참이지만 결론 가 참이 아닌 경우 로 정의된다.[34][91] 이것은 결론이 전제의 ''의미적 귀결''이라고 말하는 것과 같다.
10. 2. 구문론적 증명 체계 (Syntactic proof systems)
공식 체계를 통해 연구되는 명제 논리에서, 공식은 형식 언어의 해석을 통해 명제를 나타낸다. 형식 언어는 증명 체계의 기반이 되며, 전제로부터 결론을 도출할 수 있게 한다. 구문론적 증명 체계는 공리계, 자연 연역, 시퀀트 계산 등으로 구성된다.명제 논리는 논리식들 간의 논리적 관계를 보여주는 데 사용되며, 변형 규칙을 사용하여 "증명" 또는 "전개" 절차를 수행한다. 증명은 번호가 매겨진 여러 줄의 서술로 표현되며, 각 줄은 근거를 덧붙여 해당 논리식을 도출한다. 증명에 필요한 가정은 "전제"로 명시하여 증명의 처음 부분에 두고, 결론은 마지막 줄에 제시한다. 모든 줄의 내용이 이전 줄의 내용을 바탕으로 변형 규칙을 정확하게 적용하여 얻어진 것이면 증명이 완료된 것으로 간주한다.
명제 논리에서는 전건 긍정의 형식과 같은 추론 규칙과 공리 기본꼴을 사용한다. 명제 논리는 또 다른 함수적 완전 집합 을 사용하여 전개할 수도 있으며, 이 경우 배중률과 같은 공리 기본꼴을 사용한다.
10. 2. 1. 공리계 (Axiomatic systems)
공식 체계를 통해 연구되는 명제 논리에서, 공식은 형식 언어의 해석을 통해 명제를 나타낸다. 형식 언어는 증명 체계의 기반이 되며, 전제로부터 결론을 도출할 수 있게 한다.명제 논리의 추론 규칙과 공리 기본꼴은 다음과 같이 나타낼 수 있다. (여기서 기호 , , 는 임의의 논리식을 나타낸다.)
- 추론 규칙
- (전건 긍정의 형식)
- 공리 기본꼴
일반적으로 명제 계산은 문법적으로 올바른 표현(정식의 집합)과 표현의 일부로 이루어지는 부분집합(공리의 집합), 표현 공간 위에 이항 관계를 정의하는 변형 규칙의 집합으로 구성되는 형식적 체계이다.
표현이 논리 체계 자체로 해석될 때, 변형 규칙은 논리적 동등성을 유지하도록 주어진다. 이러한 변형 규칙을 통해 주어진 표현에서 논리적으로 동등한 표현을 도출할 수 있다.
명제 논리에서의 '언어'는 명제 변수(명제를 끼워 넣는 틀)와 문 연산자(결합자)로 이루어져 있다. 형식 문법에 의해 귀납적으로 언어의 표현이나 정식이 정의되며, 공리 도식에 의해 주어질 수 있다. 의미론에 의해 참 또는 거짓의 값 매김(또는 해석)이 정해져, 어떤 정식이 옳은지, 즉 정리인지를 결정할 수 있다.
10. 2. 2. 자연 연역 (Natural deduction)
자연 연역은 명제 논리에서 사용되는 추론 방법 중 하나이다. 자연 연역의 주요 특징과 규칙은 다음과 같다.자연 연역은 참이라고 가정한 식들로부터 다른 참인 식을 도출하는 규칙들을 사용한다. 여기에는 비가정적 규칙과 가정적 규칙 두 가지 유형이 있다.
- 비가정적 규칙:
- '''이중 부정의 제거''': ¬¬φ로부터 φ를 추론한다.
- '''합접의 도입''': φ와 ψ로부터 (φ∧ψ)를 추론한다.
- '''합접의 제거''': φ∧ψ로부터 φ와 ψ를 추론한다.
- '''선택의 도입''': φ로부터, 어떤 식 ψ에 대해서도 (φ∨ψ)와 (ψ∨φ)를 추론한다.
- '''선택의 제거''': (φ∨ψ), (φ→χ), (ψ→χ) 형태의 식으로부터 χ를 추론한다.
- '''전건긍정'''(modus ponens): φ와 (φ→ψ) 형태의 식으로부터 ψ를 추론한다.
- 가정적 규칙:
- '''조건적 증명''': φ를 가정하고 식 ψ가 도출되었다면 (φ→ψ)를 추론한다.
- '''귀류법'''(reductio ad absurdum): φ를 가정하고 ψ와 ¬ψ가 도출되었다면 ¬φ를 추론한다.
이러한 규칙들을 통해 명제 논리에서 참인 명제들로부터 새로운 참인 명제를 도출할 수 있다.
11. 진리표를 통한 의미론적 증명 (Semantic proof via truth tables)
주어진 언어 에 대해, '''해석''',[63] '''값 매김''',[48] 또는 '''경우'''[34]는 의 각 공식에 대한 의미 값의 대입이다.[34] 고전 논리의 형식 언어의 경우, 경우는 의 각 공식에 대해 진리값인 참('''T''', 또는 1)과 거짓('''F''', 또는 0) 중 하나를, 하지만 둘 다 아닌 것을 대입하는 것으로 정의된다.[64][65] 고전 논리의 규칙을 따르는 해석은 때때로 '''부울 값 매김'''이라고 한다.[48][66]
고전 논리에 대한 형식 언어의 해석은 종종 진리표를 통해 표현된다.[67][1] 각 공식에 단일 진리값만 할당되므로, 해석은 정의역이 이고 공역이 의미 값 집합 ,[2] 또는 인 함수로 볼 수 있다.[34]
개의 서로 다른 명제 기호에 대해 개의 서로 다른 가능한 해석이 있다. 예를 들어, 특정 기호 의 경우, 개의 가능한 해석이 있다. 즉, 에 '''T'''가 할당되거나 '''F'''가 할당된다. 그리고 쌍 , 의 경우, 개의 가능한 해석이 있다.[67] 이 , 즉 가산 가능한 많은 명제 기호를 가지므로, 개, 따라서 비가산 가능한 많은 서로 다른 가능한 의 해석이 있다.[67]
논리연결사는 적용되는 명제 변수가 두 가지 가능한 진릿값 중 하나를 취할 때 취하는 진릿값만으로 의미적으로 정의되기 때문에,[1][34] 연결사의 의미적 정의는 일반적으로 아래와 같이 각 연결사에 대한 진리표로 표현된다.[1][34][102]
p | q | p ∧ q | p ∨ q | p → q | p ↔ q | ¬p | ¬q |
---|---|---|---|---|---|---|---|
T | T | T | T | T | T | F | F |
T | F | F | T | F | F | F | T |
F | T | F | T | T | F | T | F |
F | F | F | F | T | T | T | T |
이 표는 주요 다섯 가지 논리연결사[13][14][15][16] 논리곱(여기서는 p ∧ q로 표기), 논리합(p ∨ q), 조건문(p → q), 논리적 동치(p ↔ q) 및 부정(¬p 또는 ¬q)를 다룬다. 이것은 이러한 연산자 각각의 의미론을 결정하기에 충분하다.[1][68][34]
12. 의미 표를 통한 의미론적 증명 (Semantic proof via tableaux)
해석적 표 분석법(analytic tableaux)은 주어진 논리식의 의미론적 참, 거짓을 판별하는 방법 중 하나이다. 이 방법은 주어진 논리식을 구성하는 명제 변수들에 진리값을 할당하고, 그 진리값에 따라 논리식 전체의 진리값이 어떻게 결정되는지를 분석한다.
주어진 언어 에 대해, 해석,[63] 값 매김,[48] 또는 경우[34]는 의 각 공식에 대한 의미 값의 대입이다.[34] 고전 논리의 형식 언어에서, 경우는 각 공식에 진리값인 참('''T''', 또는 1) 또는 거짓('''F''', 또는 0) 중 하나를 할당하는 것이다 (둘 다는 아니다).[64][65] 고전 논리의 규칙을 따르는 해석은 부울 값 매김이라고도 한다.[48][66] 고전 논리에서 형식 언어의 해석은 진리표를 통해 표현할 수 있다.[67][1] 각 공식에 단일 진리값만 할당되므로, 해석은 정의역이 이고 공역이 의미 값 집합 ,[2] 또는 인 함수로 볼 수 있다.[34]
개의 서로 다른 명제 기호에 대해 개의 서로 다른 가능한 해석이 존재한다. 예를 들어, 특정 기호 의 경우, 개의 가능한 해석 ('''T''' 또는 '''F''' 할당)이 있다. 와 쌍의 경우, 개의 가능한 해석이 존재한다.[67] 이 가산 가능한 무한 개의 명제 기호를 가지면, 개, 즉 비가산 가능한 수의 서로 다른 해석이 가능하다.[67]
가 해석이고 와 가 공식일 때, 논증은 쌍으로 나타낼 수 있다. 여기서 은 전제 집합, 는 결론이다. 논증의 ''타당성''( )은 반례가 없음으로 나타낼 수 있다. 반례는 전제 가 모두 참이지만 결론 는 참이 아닌 경우 이다.[34][91] 이는 결론이 전제의 ''의미적 귀결''임을 의미한다.
13. 자연 연역을 통한 구문적 증명 (Syntactic proof via natural deduction)
명제 논리는 논리식 간의 관계를 보여주기 위해 사용되며, "증명" 또는 "전개"라는 절차를 통해 이를 수행한다. 증명은 번호가 매겨진 여러 줄의 서술로 표현되며, 각 줄은 하나의 논리식과 그 도출 근거를 포함한다. 증명에 필요한 가정은 "전제"로 증명 처음에 명시하고, 결론은 마지막 줄에 제시한다.[1]
여기서는 여덟 가지 추론 규칙을 사용한다. 이 규칙들을 통해 참이라고 가정된 식에서 다른 참인 식을 도출할 수 있다. 처음 여섯 가지는 비가정적 규칙으로, 단순히 특정 식을 다른 식에서 도출할 수 있음을 나타낸다. 마지막 두 가지는 가정적 규칙으로, 증명되지 않은 가정을 일시적으로 사용한다.
- 이중 부정의 제거: 식 ¬¬φ로부터 φ를 추론할 수 있다.
- 합접의 도입: 식 φ와 식 ψ로부터 (φ∧ψ)를 추론할 수 있다.
- 합접의 제거: 식 φ∧ψ로부터 φ와 ψ를 추론할 수 있다.
- 선택의 도입: 식 φ로부터, 어떤 식 ψ에 대해서도 (φ∨ψ)와 (ψ∨φ)를 추론할 수 있다.
- 선택의 제거: (φ∨ψ), (φ→χ), (ψ→χ) 형태의 식으로부터 χ를 추론할 수 있다.
- 전건긍정: φ와 (φ→ψ) 형태의 식으로부터 ψ를 추론할 수 있다.
- 조건적 증명: φ를 가정하고 식 ψ가 도출되었다면 (φ→ψ)를 추론할 수 있다.
- 귀류법: φ를 가정하고 ψ와 ¬ψ가 도출되었다면 ¬φ를 추론할 수 있다.
아래는 를 증명하는 예시이다. (더 엄밀한 증명에는 더 많은 단계가 필요하다.)
행 번호 | 식 | 근거 |
---|---|---|
1 | 가정 | |
2 | 1, 논리합의 도입 | |
3 | 1, 2, 논리곱의 도입 | |
4 | 3, 논리곱의 제거 | |
5 | 1, 4, 조건부 증명 |
13. 1. 표기법 스타일 (Notation styles)
주어진 `source`는 명제 논리의 일반적인 내용을 설명하고 있으며, "표기법 스타일"에 대한 구체적인 정보를 포함하고 있지 않습니다. 따라서 이전 답변과 동일하게, 주어진 `source`만으로는 "표기법 스타일" 섹션을 작성할 수 없습니다. `summary`에서 요구하는 겐첸 표기법, 야스코프스키 스타일 등에 대한 내용은 `source`에 없으므로, 해당 내용을 추가하는 것은 불가능합니다.결론적으로, 이전 답변을 수정할 내용이 없습니다.
13. 2. 추론 규칙 (Inference rules)
규칙 | 설명 |
---|---|
이중 부정의 제거 | 식 ¬¬φ로부터 φ를 추론할 수 있다. |
합접의 도입 | 식 φ와 식 ψ로부터 (φ∧ψ)를 추론할 수 있다. |
합접의 제거 | 식 φ∧ψ로부터 φ와 ψ를 추론할 수 있다. |
선택의 도입 | 식 φ로부터, 어떤 식 ψ에 대해서도 (φ∨ψ)와 (ψ∨φ)를 추론할 수 있다. |
선택의 제거 | (φ∨ψ), (φ→χ), (ψ→χ) 형태의 식으로부터 χ를 추론할 수 있다. |
전건긍정 | φ와 (φ→ψ) 형태의 식으로부터 ψ를 추론할 수 있다. |
조건적 증명 | φ를 가정하고 식 ψ가 도출되었다면 (φ→ψ)를 추론할 수 있다. |
귀류법 | φ를 가정하고 ψ와 ¬ψ가 도출되었다면 ¬φ를 추론할 수 있다. |
처음 여섯 가지 규칙은 비가정적 규칙이고, 마지막 두 가지는 가정적 규칙이다.[1]
13. 3. 자연 연역 증명 예시 (Natural deduction proof example)
Natural deduction proof example영어에서는 모두스 포넨스와 귀류법만을 사용하여 "P → Q"와 "-Q"로부터 "-P"를 유도하는 증명 예시를 제시한다.명제논리는 주로 논리식들 간의 논리적 관계를 보여주는 데 사용된다. 이를 위해 사용 가능한 (논리식의) 변형 규칙을 사용하여 “증명” 또는 “전개”라고 하는 절차를 수행한다. 증명은 번호가 매겨진 여러 줄의 서술로 표현된다. 각 줄은 근거 또는 이유를 덧붙여 해당 논리식을 도출하기 위한 단일 논리식으로 한다. 증명에 필요한 가정은 “전제”로 명시하여 증명의 처음 부분에 둔다. 결론은 마지막 줄에 제시한다. 모든 줄의 내용이 그 이전 줄의 내용을 바탕으로 (논리식의) 변형 규칙을 정확하게 적용하여 얻어진 것이면 증명이 완료된 것으로 간주한다. (참고로, 테이블로 방법이라는 다른 서술 방법도 있다.)
- ''A'' → ''A''를 증명한다.
- 아래에 그 증명의 한 예를 든다(더 엄밀하게 증명하려면 더 많은 단계가 필요하다).
증명의 예 | ||
---|---|---|
행 번호 | 식 | 근거 |
1 | 가정 | |
2 | 1, 논리합의 도입 | |
3 | 1, 2, 논리곱의 도입 | |
4 | 3, 논리곱의 제거 | |
5 | 1, 4, 조건부 증명 |
14. 공리를 통한 구문적 증명 (Syntactic proof via axioms)
명제 논리는 공식 체계를 통해 연구되며, 공식은 형식 언어의 해석을 통해 명제를 나타낸다. 이 형식 언어는 증명 체계의 기반이 되며, 전제로부터 결론을 도출할 수 있게 한다.
명제 논리에서 주로 다루는 것은 개별 명제의 의미보다는, 명제들을 논리 연산자를 통해 연결했을 때 어떤 추론이 가능한가 하는 것이다. 개별 명제의 의미는 술어 논리 등에서 다룬다.
직관주의 논리, 양상 논리, 상관 논리 등 다양한 명제 논리가 있지만, 보통 명제 논리라고 하면 고전 명제 논리를 가리킨다.[121]
명제 계산은 일반적으로 "문법적으로 괜찮은" 통어적인 표현(정식의 집합)과 그 표현의 일부로 이루어지는 부분집합(공리의 집합), 그리고 표현의 공간 위에 이항 관계를 정의하는 변형 규칙의 집합으로 이루어진다.
각 표현이 수학적 표현으로 해석될 때, 표현의 변형 규칙은 일정한 의미 동등성을 유지하도록 주어지며, 특히 표현이 논리 체계 자체로 해석될 때는 "의미 동등성"이 논리적 동등성을 가리키도록 변형 규칙이 주어진다. 이러한 변형 규칙을 통해 주어진 표현으로부터 논리적으로 동등한 표현을 도출할 수 있다.
명제 논리에서의 ''언어''는 명제 변수(명제를 끼워 넣는 틀)와 문연산자(결합자)로 이루어져 있으며, 형식 문법에 의해 귀납적으로 정의된다. 공리의 집합은 공집합, 유한 집합, 가산 무한 집합일 수 있으며, 공리 도식으로 주어질 수도 있다. 의미론에 의해 참 또는 거짓의 값 매김(해석)이 정해지고, 이를 통해 어떤 정식이 정리인지를 결정할 수 있다.
명제 논리는 주로 논리식들 간의 논리적 관계를 보여주기 위해 사용되며, "증명" 또는 "전개"라는 절차를 수행한다. 증명은 번호가 매겨진 여러 줄의 서술로 표현되며, 각 줄은 근거와 함께 단일 논리식을 포함한다. 전제는 증명의 처음에 명시하고, 결론은 마지막 줄에 제시한다. 모든 줄의 내용이 이전 줄의 내용을 바탕으로 변형 규칙을 정확하게 적용하여 얻어진 것이면 증명이 완료된 것으로 간주한다.
- 증명 예시:
증명의 예 | ||
---|---|---|
행 번호 | 식 | 근거 |
1 | 가정 | |
2 | 1, 논리합의 도입 | |
3 | 1, 2, 논리곱의 도입 | |
4 | 3, 논리곱의 제거 | |
5 | 1, 4, 조건부 증명 |
14. 1. 프레게의 개념 기호법 (Frege's Begriffsschrift)
고틀로브 프레게의 술어 논리는 명제 논리를 기반으로 하며, "삼단 논리와 명제 논리의 독특한 특징을 결합한 것"으로 묘사되었다.[24] 프레게는 명제 논리 체계를 제시하면서 공리와 추론 규칙을 사용했다.스티븐 콜 클라인(Stephen Cole Kleene)이 제시한 명제 논리 체계[122]는 11개의 공리와 하나의 추론 규칙을 사용한다.
이름 | 공리 | 비고 |
---|---|---|
THEN-1 | 함의 도입[123] | |
THEN-2 | 함의의 추이성, 프레게의 삼단논법[124] | |
AND-1 | 논리곱 소거, 단순화[125] | |
AND-2 | 논리곱 소거 | |
AND-3 | 논리곱 도입 | |
OR-1 | 논리합 도입 | |
OR-2 | 논리합 도입 | |
OR-3 | ||
NOT-1 | 귀류법 | |
NOT-2 | 폭발률 (모순에서 무엇이든 도출 가능) | |
NOT-3 | 배중률 |
- AND-1, AND-2는 논리곱의 교환 법칙을 반영한다.
- OR-1, OR-2는 논리합의 교환 법칙을 반영한다.
- NOT-2를 제한하여 논리 체계를 구성하는 방법을 모순 허용 논리라 한다.
- NOT-3은 식의 진릿값이 참 또는 거짓 중 하나임을 나타낸다. 고전 논리학에서는 세 번째 진릿값을 고려하지 않는다. NOT-3을 인정하지 않는 논리 체계는 직관주의 논리이다.
클라인 체계의 유일한 추론 규칙은 모드스 포넨스이다. 즉,
: 와 형태의 식에서 를 추론할 수 있다.
다비트 힐베르트(David Hilbert)는 다음과 같은 공리계를 제시했다.
힐베르트 체계의 추론 규칙 역시 모더스 포넨스이다. 즉, “ 와 로부터 를 추론할 수 있다”는 것이다.
이 공리계에서 “”와 “”는 각각 “”와 “”의 약어로 간주한다.
14. 2. 우카셰비치의 P₂ (Łukasiewicz's P₂)
얀 우카셰비치는 다음 세 공리와 모드스 포넨스(modus ponens), 치환 규칙을 포함하는 명제 논리 체계(P₂)를 제시했다.여기서 “”와 “”는 각각 “”와 “”의 약어로 간주된다.
알론조 처치는 P₂라는 명칭으로 힐베르트 공리계와 동일한 체계를 사용하였다.[126]
14. 2. 1. P₂의 도식적 형태 (Schematic form of P₂)
스티븐 콜 클레이니(Stephen Cole Kleene)가 제시한 체계[122]는 11개의 공리와 하나의 추론 규칙을 사용한다.이름 | 공리 | 비고 |
---|---|---|
THEN-1 | 함의 도입[123]이라고 일반적으로 부른다. | |
THEN-2 | 「함의의 추이성」에 대응한다. 프레게의 삼단논법[124]이라고 일반적으로 부른다. | |
AND-1 | 「논리곱의 소거」에 대응한다. 단순화[125]라고 부른다. | |
AND-2 | 「논리곱의 소거」에 대응한다. | |
AND-3 | 「논리곱의 도입」에 대응한다. | |
OR-1 | 「논리합의 도입」에 대응한다. | |
OR-2 | 「논리합의 도입」에 대응한다. | |
OR-3 | ||
NOT-1 | 「귀류법」에 대응한다. | |
NOT-2 | 「폭발의 원리(principle of explosion) 모순으로부터 무엇이든지 도출할 수 있다」. | |
NOT-3 | 「배중률」. |
- 공리 AND-1과 공리 AND-2의 평행성은 논리곱의 교환 법칙을 반영하고 있다.
- 공리 OR-1과 공리 OR-2의 평행성은 논리합의 교환 법칙을 반영하고 있다.
- 공리 NOT-2에 어떤 제한을 더하여 논리 체계를 구성하는 방법을 모순 허용 논리라고 부른다.
- 공리 NOT-3은 명제식의 의미론적 값 매김의 가능성을 반영하고 있다. 식의 진릿값은 참 또는 거짓 중 하나이다. 적어도 고전 논리학에서는 세 번째 진릿값이라는 가능성은 고려되지 않는다. 공리 NOT-3을 인정하지 않고 논리 체계를 구성하는 방법을 직관주의 논리라고 부른다.
추론 규칙은 모드스 포넨스 즉,
: 와 와 같은 형태의 정식으로부터 를 추론할 수 있다는 것만을 규정한다. 위의 공리계와 이 추론 규칙으로부터 #추론규칙 절에서 설명된 것과 같은 연역이 가능해진다.
15. 더 높은 논리 수준 (Higher logical levels)
일차 술어 논리는 명제 논리의 "원시적 서술"을 항, 변수, 술어, 양화자로 분해하여, 명제 논리의 규칙을 모두 유지하면서 새로운 규칙을 추가한 것이다. 예를 들어, "모든 고양이는 포유류이다"에서 "타마가 고양이라면, 타마는 포유류이다"를 추론할 수 있다.[119]
일차 논리를 활용하면 공리나 추론 규칙을 통해 다양한 이론을 공식화하고 논리 계산으로 다룰 수 있다. 대표적인 예시로는 산술이 있으며, 그 외에도 집합론이나 메레올로지 등이 있다.[120]
양상 논리는 명제 논리로는 파악하기 어려운 다양한 추론을 가능하게 한다. 예를 들어, 양상 논리에서는 "는 필연적이다"에서 를 추론할 수 있고, 에서 "는 가능하다"를 추론할 수 있다.[121]
다치 논리는 문장의 진리값으로 참과 거짓 외에 다른 값도 허용한다. 예를 들어, "참이기도 하고 거짓이기도 하다" 또는 "참도 아니고 거짓도 아니다"와 같은 값을 추가할 수 있다. 퍼지 논리에서는 참과 거짓 사이에 무한히 미세한 "참인 정도"를 도입하기도 한다. 이러한 논리 체계에서는 명제 논리와 다른 계산 방법이 필요한 경우가 많다.
16. 관련 주제 (Related topics)
```
이전 출력과 비교했을 때 변경된 사항은 없습니다. 모든 지시사항을 완벽하게 준수하고 있습니다.
참조
[1]
웹사이트
Propositional Logic Internet Encyclopedia of Philosophy
https://iep.utm.edu/[...]
2024-03-22
[2]
논문
Propositional Logic
https://plato.stanfo[...]
Metaphysics Research Lab, Stanford University
2024-03-22
[3]
웹사이트
Propositional Calculus
https://mathworld.wo[...]
2024-03-22
[4]
서적
Principles of Mathematical Logic
Chelsea Publishing Company
[5]
논문
An epsilon of room, II
American Mathematical Society
[6]
서적
An introduction to mathematical logic and type theory: to truth through proof
https://books.google[...]
Kluwer Academic Publishers, Dordrecht
[7]
서적
Fuzzy logic and mathematics: a historical perspective
Oxford University Press
2017
[8]
서적
Extensions of first order logic
Cambridge University Press
2005
[9]
서적
Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types
https://books.google[...]
Herbert Utz Verlag
1999
[10]
논문
Propositions
https://plato.stanfo[...]
Metaphysics Research Lab, Stanford University
2024-03-22
[11]
웹사이트
Predicate Logic
https://www3.cs.ston[...]
2024-03-22
[12]
웹사이트
Philosophy 404: Lecture Five
https://www.webpages[...]
2024-03-22
[13]
웹사이트
3.1 Propositional Logic
https://www.teach.cs[...]
2024-03-22
[14]
서적
Semantics: a reader
Oxford University Press
2004
[15]
서적
Elements of logical reasoning
Cambridge University press
2013
[16]
웹사이트
Propositional Logic
https://www.cs.miami[...]
2024-03-22
[17]
서적
Elements of logical reasoning
Cambridge University press
2013
[18]
웹사이트
Connective
https://mathworld.wo[...]
2024-03-22
[19]
웹사이트
Propositional Logic Brilliant Math & Science Wiki
https://brilliant.or[...]
2020-08-20
[20]
논문
The Stanford Encyclopedia of Philosophy
http://plato.stanfor[...]
Metaphysics Research Lab, Stanford University
2016-01-01
[21]
웹사이트
Propositional Logic Internet Encyclopedia of Philosophy
https://iep.utm.edu/[...]
2020-08-20
[22]
논문
Ancient Logic
https://plato.stanfo[...]
Metaphysics Research Lab, Stanford University
2024-03-22
[23]
논문
The Stanford Encyclopedia of Philosophy
http://plato.stanfor[...]
Metaphysics Research Lab, Stanford University
2014-01-01
[24]
서적
A Concise Introduction to Logic 10th edition
Wadsworth Publishing
[25]
간행물
The Philosophy of Mathematics
Oxford University Press
[26]
웹사이트
Truth in Frege
https://web.archive.[...]
[27]
웹사이트
Russell: the Journal of Bertrand Russell Studies
http://digitalcommon[...]
[28]
학술지
Peirce's Truth-functional Analysis and the Origin of the Truth Table
2012
[29]
웹사이트
Part2Mod1: LOGIC: Statements, Negations, Quantifiers, Truth Tables
https://www.math.fsu[...]
2024-03-22
[30]
웹사이트
Lecture Notes on Logical Organization and Critical Thinking
https://www2.hawaii.[...]
2024-03-22
[31]
웹사이트
Logical Connectives
https://sites.miller[...]
2024-03-22
[32]
웹사이트
Lecture1
https://www.cs.colum[...]
2024-03-22
[33]
웹사이트
Introduction to Logic - Chapter 2
http://intrologic.st[...]
2024-03-22
[34]
서적
Logic: the basics
Routledge
2010
[35]
웹사이트
Watson
http://watson.latech[...]
2024-03-22
[36]
웹사이트
Introduction to Theoretical Computer Science, Chapter 1
https://www.cs.odu.e[...]
2024-03-22
[37]
서적
Logic primer
The MIT Press
2022
[38]
논문
One's Modus Ponens: Modality, Coherence and Logic
https://www.jstor.or[...]
2017
[39]
백과사전
Argument and Argumentation
https://plato.stanfo[...]
Metaphysics Research Lab, Stanford University
2024-04-05
[40]
웹사이트
Validity and Soundness Internet Encyclopedia of Philosophy
https://iep.utm.edu/[...]
2024-04-05
[41]
백과사전
Natural Deduction Systems in Logic
https://plato.stanfo[...]
Metaphysics Research Lab, Stanford University
2024-03-22
[42]
백과사전
Substructural Logics
https://plato.stanfo[...]
Metaphysics Research Lab, Stanford University
2024-03-22
[43]
웹사이트
Compactness Internet Encyclopedia of Philosophy
https://iep.utm.edu/[...]
2024-03-22
[44]
웹사이트
Lecture Topics for Discrete Math Students
https://math.colorad[...]
2024-03-22
[45]
백과사전
Deductivism in the Philosophy of Mathematics
https://plato.stanfo[...]
Metaphysics Research Lab, Stanford University
2024-03-22
[46]
백과사전
Logic and Probability
https://plato.stanfo[...]
Metaphysics Research Lab, Stanford University
2024-03-22
[47]
서적
Mathematical logic
Dover Publications
2002
[48]
서적
First-order logic
Dover
1995
[49]
서적
The connectives
https://www.worldcat[...]
MIT Press
2011
[50]
서적
Principles of mathematics
Routledge
2010
[51]
서적
Logic
Penguin
1977
[52]
서적
Introduction to formal philosophy
Springer
2018
[53]
서적
Applied Logic for Computer Scientists
https://link.springe[...]
Springer
2017
[54]
서적
Classical logic and its rabbit holes: a first course
Hackett Publishing Co., Inc
2013
[55]
서적
Intermediate logic
Clarendon Press; Oxford University Press
1997
[56]
서적
Propositional and predicate calculus: a model of argument
Springer
2005
[57]
웹사이트
Propositional Logic
https://www.cs.roche[...]
2024-03-22
[58]
웹사이트
Propositional calculus
https://www.cs.corne[...]
2024-03-22
[59]
백과사전
Truth Values
https://plato.stanfo[...]
Metaphysics Research Lab, Stanford University
2024-03-23
[60]
논문
Should doctors spurn Wikipedia?
2011
[61]
서적
How Wikipedia works: and how you can be a part of it
https://www.worldcat[...]
No Starch Press
2008
[62]
백과사전
Classical Logic
https://plato.stanfo[...]
Metaphysics Research Lab, Stanford University
2024-03-25
[63]
논문
Structures for Semantics
https://doi.org/10.1[...]
1991
[64]
서적
Frontiers in quantum methods and applications in chemistry and physics: selected proceedings of QSCP-XVIII (Paraty, Brazil, December, 2013)
Springer
2015
[65]
논문
Fundamentals of Artificial Intelligence
https://doi.org/10.1[...]
2020
[66]
서적
Logical Methods
https://books.google[...]
MIT Press
2023-01-03
[67]
서적
Metalogic: An Introduction to the Metatheory of Standard First-Order Logic
University of California Press
[68]
백과사전
Disjunction
https://plato.stanfo[...]
Metaphysics Research Lab, Stanford University
2024-03-23
[69]
서적
Symbolic logic
Palgrave Macmillan
2022
[70]
서적
Philosophical logic
https://www.worldcat[...]
Princeton University Press
2009
[71]
서적
Logical Pluralism
https://books.google[...]
Clarendon Press
2006
[72]
서적
Propositional Logic
https://discrete.ope[...]
[73]
간행물
An introduction to formal logic
Cambridge University Press
[74]
서적
Set theory: a first course
Cambridge University Press
2016
[75]
서적
Introduction to Logic
https://link.springe[...]
Springer International Publishing
2017
[76]
웹사이트
6. Semantics of Propositional Logic — Logic and Proof 3.18.4 documentation
https://leanprover.g[...]
2024-03-28
[77]
웹사이트
Knowledge Representation and Reasoning: Basics of Logics
https://www.emse.fr/[...]
2024-03-28
[78]
서적
Computational logic in multi-agent systems: 10th international workshop, CLIMA X, Hamburg, Germany, September 9-10, 2009: revised selected and invited papers
https://www.worldcat[...]
Springer
2010
[79]
서적
Computational models of argument: proceedings of comma 2020
IOS Press
2020
[80]
서적
Mathematical Logic and Formalized Theories
http://dx.doi.org/10[...]
Elsevier
1971
[81]
서적
Rudolf carnap: studies in semantics: the collected works of rudolf carnap, volume 7
Oxford University Press
2024
[82]
서적
Advances in Mathematics Education Research on Proof and Proving: An International Perspective
Springer International Publishing : Imprint: Springer
2018
[83]
학술지
A Concise Introduction to Logic: §4. Proofs
https://milnepublish[...]
2024-03-23
[84]
간행물
semantic consequence
https://www.oxfordre[...]
Oxford University Press
2024-03-23
[85]
간행물
syntactic consequence
https://www.oxfordre[...]
Oxford University Press
2024-03-23
[86]
서적
A dictionary of philosophical logic
Edinburgh University Press
2009
[87]
웹사이트
Truth table {{!}} Boolean, Operators, Rules {{!}} Britannica
https://www.britanni[...]
2024-03-23
[88]
웹사이트
MathematicalLogic
https://www.cs.yale.[...]
2024-03-23
[89]
웹사이트
Analytic Tableaux
https://www3.cs.ston[...]
2024-03-23
[90]
웹사이트
Formal logic - Semantic Tableaux, Proofs, Rules {{!}} Britannica
https://www.britanni[...]
2024-03-23
[91]
서적
Logic with trees: an introduction to symbolic logic
Routledge
1997
[92]
웹사이트
Axiomatic method {{!}} Logic, Proofs & Foundations {{!}} Britannica
https://www.britanni[...]
2024-03-23
[93]
웹사이트
Propositional Logic
https://mally.stanfo[...]
2024-03-23
[94]
웹사이트
Natural Deduction {{!}} Internet Encyclopedia of Philosophy
https://iep.utm.edu/[...]
2024-03-23
[95]
웹사이트
Sequent Calculus
https://mathworld.wo[...]
2024-03-23
[96]
웹사이트
Interactive Tutorial of the Sequent Calculus
http://logitext.mit.[...]
2024-03-23
[97]
웹사이트
1.4: Tautologies and contradictions
https://math.librete[...]
2024-03-29
[98]
서적
EF Tautologies and contradictions
https://sites.ualber[...]
[99]
서적
Elementary Formal Logic
https://intrologicim[...]
Pressbooks
[100]
서적
Principles of expert systems
https://www.cs.ru.nl[...]
Addison-Wesley
1991
[101]
웹사이트
CSE541 Logic in Computer Science
https://www3.cs.ston[...]
2009
[102]
서적
Logic: an introduction
Routledge
2010
[103]
서적
A first course in logic
CRC Press, Taylor & Francis Group
2019
[104]
서적
Logic and language
Palgrave Macmillan
2003
[105]
서적
Mathematical logic
Oxford university press
2007
[106]
서적
Logic
Penguin Books
2001
[107]
웹사이트
Proof of Implications
http://www.cs.odu.ed[...]
Department of Computer Science, Old Dominion University
2009-08-02
[108]
서적
Beginning logic
Chapman & Hall/CRC
1998
[109]
웹사이트
Natural Deduction Systems in Logic > Notes (Stanford Encyclopedia of Philosophy)
https://plato.stanfo[...]
2024-04-19
[110]
서적
An introduction to logic: using natural deduction, real arguments, a little history, and some humour
https://www.worldcat[...]
Broadview Press
2017
[111]
서적
A Beginner's Guide to Mathematical Logic
https://books.google[...]
Courier Corporation
2014-07-23
[112]
서적
The Philosophy of Gottlob Frege
https://books.google[...]
Cambridge University Press
2005-01-10
[113]
서적
Jan Lukasiewicz: Selected Works
https://books.google[...]
North-Holland
1970
[114]
서적
Introduction to Mathematical Logic
https://books.google[...]
Princeton University Press
1996
[115]
웹사이트
Proof Explorer - Home Page - Metamath
https://us.metamath.[...]
2024-07-02
[116]
서적
Introduction to mathematical logic
World Scientific
2017
[117]
서적
Mathematical Logic
Harvard University Press
1980
[118]
웹사이트
命題論理
https://kotobank.jp/[...]
[119]
용어
propositional calculus
[120]
용어
sentential calculus
[121]
용어
classical propositional logic
[122]
서적
Introduction to Metamathematics
North Holland
1967
[123]
용어
introduction of implication
[124]
용어
Fregean syllogism
[125]
용어
simplification
[126]
용어
weakening
[127]
용어
contraction
[128]
용어
permutation
[129]
서적
A Course on Mathematical Logic
https://archive.org/[...]
Springer
2008
[130]
저널
Complete Sets of Logical Functions
1942-01
본 사이트는 AI가 위키백과와 뉴스 기사,정부 간행물,학술 논문등을 바탕으로 정보를 가공하여 제공하는 백과사전형 서비스입니다.
모든 문서는 AI에 의해 자동 생성되며, CC BY-SA 4.0 라이선스에 따라 이용할 수 있습니다.
하지만, 위키백과나 뉴스 기사 자체에 오류, 부정확한 정보, 또는 가짜 뉴스가 포함될 수 있으며, AI는 이러한 내용을 완벽하게 걸러내지 못할 수 있습니다.
따라서 제공되는 정보에 일부 오류나 편향이 있을 수 있으므로, 중요한 정보는 반드시 다른 출처를 통해 교차 검증하시기 바랍니다.
문의하기 : help@durumis.com